(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 25) (_ BitVec 12) (_ BitVec 110)) (_ BitVec 110))
(declare-fun p0 ( (_ BitVec 7)) Bool)
(declare-fun p1 ( (_ BitVec 63) (_ BitVec 31)) Bool)
(declare-fun v0 () (_ BitVec 127))
(declare-fun v1 () (_ BitVec 87))
(declare-fun v2 () (_ BitVec 2))
(declare-fun v3 () (_ BitVec 31))
(assert (let ((e4(_ bv123990754665941515940477959765080456645 128)))
(let ((e5(_ bv3602565890429738 53)))
(let ((e6 (f0 ((_ extract 24 0) v1) ((_ extract 75 64) e4) ((_ sign_extend 79) v3))))
(let ((e7 (ite (p1 ((_ extract 90 28) v0) v3) (_ bv1 1) (_ bv0 1))))
(let ((e8 (ite (p0 ((_ sign_extend 5) v2)) (_ bv1 1) (_ bv0 1))))
(let ((e9 (ite (bvult e6 ((_ zero_extend 109) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e10 ((_ extract 68 57) v0)))
(let ((e11 (ite (= (_ bv1 1) ((_ extract 1 1) v2)) e6 ((_ zero_extend 109) e9))))
(let ((e12 (bvsub ((_ sign_extend 108) v2) e11)))
(let ((e13 (bvneg e4)))
(let ((e14 (bvsdiv ((_ sign_extend 126) v2) e13)))
(let ((e15 (ite (distinct ((_ zero_extend 41) v1) e14) (_ bv1 1) (_ bv0 1))))
(let ((e16 ((_ rotate_right 10) e10)))
(let ((e17 (bvcomp e11 ((_ zero_extend 109) e8))))
(let ((e18 ((_ sign_extend 16) e17)))
(let ((e19 ((_ sign_extend 0) v0)))
(let ((e20 (bvmul ((_ zero_extend 19) e10) v3)))
(let ((e21 ((_ rotate_left 49) e12)))
(let ((e22 (ite (distinct ((_ zero_extend 127) e15) e13) (_ bv1 1) (_ bv0 1))))
(let ((e23 (f0 ((_ zero_extend 24) e15) ((_ zero_extend 11) e22) ((_ zero_extend 23) v1))))
(let ((e24 (bvashr e23 e6)))
(let ((e25 (ite (bvule v1 ((_ sign_extend 86) e22)) (_ bv1 1) (_ bv0 1))))
(let ((e26 (bvmul e13 ((_ zero_extend 127) e15))))
(let ((e27 (ite (bvslt ((_ zero_extend 116) e16) e13) (_ bv1 1) (_ bv0 1))))
(let ((e28 ((_ rotate_right 0) e17)))
(let ((e29 (bvmul e19 ((_ zero_extend 40) v1))))
(let ((e30 (bvor ((_ sign_extend 126) e15) v0)))
(let ((e31 (bvor e14 ((_ sign_extend 1) e19))))
(let ((e32 (bvshl e31 ((_ sign_extend 18) e11))))
(let ((e33 (ite (bvsgt ((_ zero_extend 19) e10) e20) (_ bv1 1) (_ bv0 1))))
(let ((e34 (ite (= ((_ sign_extend 18) e23) e4) (_ bv1 1) (_ bv0 1))))
(let ((e35 (f0 ((_ extract 56 32) e24) ((_ sign_extend 11) e8) ((_ extract 117 8) v0))))
(let ((e36 (bvor e30 e19)))
(let ((e37 (ite (p0 ((_ zero_extend 6) e25)) (_ bv1 1) (_ bv0 1))))
(let ((e38 ((_ sign_extend 51) e18)))
(let ((e39 ((_ rotate_left 98) e11)))
(let ((e40 (bvnor e26 ((_ zero_extend 18) e11))))
(let ((e41 (f0 ((_ zero_extend 24) e9) ((_ zero_extend 11) e28) ((_ zero_extend 42) e38))))
(let ((e42 (bvlshr e22 e33)))
(let ((e43 (bvor e15 e8)))
(let ((e44 (bvand e12 ((_ zero_extend 57) e5))))
(let ((e45 (p0 ((_ extract 30 24) e21))))
(let ((e46 (bvsle e13 ((_ sign_extend 127) e8))))
(let ((e47 (p1 ((_ extract 106 44) e41) v3)))
(let ((e48 (distinct e31 ((_ zero_extend 18) e12))))
(let ((e49 (distinct e36 ((_ zero_extend 96) v3))))
(let ((e50 (bvuge e13 ((_ sign_extend 127) e7))))
(let ((e51 (bvuge ((_ sign_extend 109) e43) e35)))
(let ((e52 (bvule e32 ((_ zero_extend 127) e43))))
(let ((e53 (bvult e7 e17)))
(let ((e54 (bvule ((_ sign_extend 18) e44) e14)))
(let ((e55 (= e19 ((_ zero_extend 126) e28))))
(let ((e56 (distinct e36 ((_ zero_extend 110) e18))))
(let ((e57 (bvugt e40 ((_ sign_extend 18) e6))))
(let ((e58 (bvslt e9 e34)))
(let ((e59 (distinct e38 ((_ zero_extend 56) e16))))
(let ((e60 (= e36 ((_ sign_extend 17) e35))))
(let ((e61 (bvsge v1 ((_ sign_extend 86) e8))))
(let ((e62 (bvsge e4 ((_ zero_extend 116) e16))))
(let ((e63 (bvslt e4 e31)))
(let ((e64 (bvuge e32 ((_ sign_extend 127) e28))))
(let ((e65 (p1 ((_ extract 93 31) e31) ((_ extract 44 14) e5))))
(let ((e66 (distinct e43 e25)))
(let ((e67 (bvsgt e23 ((_ sign_extend 109) e8))))
(let ((e68 (bvsgt e7 e25)))
(let ((e69 (p0 ((_ extract 36 30) e40))))
(let ((e70 (p0 ((_ extract 30 24) e35))))
(let ((e71 (bvslt ((_ zero_extend 1) e36) e40)))
(let ((e72 (bvsgt ((_ zero_extend 67) e28) e38)))
(let ((e73 (bvule ((_ sign_extend 40) v1) e30)))
(let ((e74 (bvsgt e40 e26)))
(let ((e75 (bvuge e6 ((_ zero_extend 109) e27))))
(let ((e76 (bvuge e32 ((_ sign_extend 75) e5))))
(let ((e77 (bvule e19 ((_ zero_extend 126) e7))))
(let ((e78 (bvuge e39 e12)))
(let ((e79 (bvsle ((_ zero_extend 18) e11) e13)))
(let ((e80 (bvsge e12 ((_ zero_extend 109) e15))))
(let ((e81 (= v0 ((_ zero_extend 126) e42))))
(let ((e82 (bvsgt e20 ((_ sign_extend 29) v2))))
(let ((e83 (distinct ((_ sign_extend 93) e18) e41)))
(let ((e84 (bvsgt e13 ((_ sign_extend 127) e7))))
(let ((e85 (bvule ((_ zero_extend 1) v0) e31)))
(let ((e86 (bvsle e25 e15)))
(let ((e87 (bvuge e26 ((_ sign_extend 116) e10))))
(let ((e88 (bvsgt ((_ sign_extend 109) e15) e41)))
(let ((e89 (bvugt ((_ zero_extend 17) e44) e29)))
(let ((e90 (bvslt e39 ((_ zero_extend 108) v2))))
(let ((e91 (bvule e19 ((_ sign_extend 126) e42))))
(let ((e92 (bvsge ((_ zero_extend 126) e22) v0)))
(let ((e93 (bvult ((_ sign_extend 127) e34) e31)))
(let ((e94 (bvsge e15 e43)))
(let ((e95 (bvugt e32 ((_ zero_extend 1) e36))))
(let ((e96 (p1 ((_ extract 93 31) e23) ((_ extract 72 42) e39))))
(let ((e97 (bvuge e12 e11)))
(let ((e98 (bvule ((_ sign_extend 18) e21) e32)))
(let ((e99 (bvuge e13 e32)))
(let ((e100 (bvugt ((_ zero_extend 16) e15) e18)))
(let ((e101 (= e6 ((_ sign_extend 109) e15))))
(let ((e102 (distinct ((_ sign_extend 57) e5) e24)))
(let ((e103 (= e21 ((_ sign_extend 93) e18))))
(let ((e104 (bvult e31 ((_ zero_extend 1) v0))))
(let ((e105 (bvult ((_ zero_extend 52) e33) e5)))
(let ((e106 (distinct ((_ sign_extend 93) e18) e35)))
(let ((e107 (bvuge ((_ sign_extend 75) e5) e14)))
(let ((e108 (bvsle ((_ zero_extend 109) e9) e12)))
(let ((e109 (distinct ((_ zero_extend 67) e22) e38)))
(let ((e110 (bvule e30 ((_ zero_extend 17) e21))))
(let ((e111 (bvugt ((_ zero_extend 127) e28) e4)))
(let ((e112 (= v3 ((_ zero_extend 19) e16))))
(let ((e113 (p1 ((_ sign_extend 32) e20) ((_ zero_extend 30) e8))))
(let ((e114 (= ((_ zero_extend 109) e33) e11)))
(let ((e115 (bvult e29 ((_ zero_extend 126) e28))))
(let ((e116 (= e31 ((_ zero_extend 127) e17))))
(let ((e117 (bvult ((_ sign_extend 109) e7) e35)))
(let ((e118 (bvugt ((_ zero_extend 18) e21) e4)))
(let ((e119 (bvsgt e31 ((_ zero_extend 127) e15))))
(let ((e120 (bvsge e12 e12)))
(let ((e121 (= e24 ((_ sign_extend 93) e18))))
(let ((e122 (distinct e39 ((_ zero_extend 109) e9))))
(let ((e123 (bvsle e13 ((_ zero_extend 1) v0))))
(let ((e124 (bvsge ((_ zero_extend 127) e17) e40)))
(let ((e125 (= e7 e25)))
(let ((e126 (bvslt ((_ zero_extend 127) e37) e4)))
(let ((e127 (not e57)))
(let ((e128 (=> e114 e108)))
(let ((e129 (= e46 e102)))
(let ((e130 (and e113 e83)))
(let ((e131 (xor e118 e115)))
(let ((e132 (not e55)))
(let ((e133 (= e100 e94)))
(let ((e134 (and e86 e79)))
(let ((e135 (not e106)))
(let ((e136 (not e125)))
(let ((e137 (not e110)))
(let ((e138 (=> e132 e67)))
(let ((e139 (xor e135 e122)))
(let ((e140 (=> e131 e53)))
(let ((e141 (and e134 e121)))
(let ((e142 (not e112)))
(let ((e143 (ite e136 e126 e142)))
(let ((e144 (=> e104 e138)))
(let ((e145 (=> e139 e130)))
(let ((e146 (not e123)))
(let ((e147 (= e75 e47)))
(let ((e148 (and e70 e96)))
(let ((e149 (ite e80 e109 e120)))
(let ((e150 (= e148 e73)))
(let ((e151 (=> e89 e49)))
(let ((e152 (or e141 e74)))
(let ((e153 (ite e95 e87 e116)))
(let ((e154 (not e124)))
(let ((e155 (or e111 e66)))
(let ((e156 (or e154 e105)))
(let ((e157 (xor e156 e119)))
(let ((e158 (or e84 e127)))
(let ((e159 (not e69)))
(let ((e160 (=> e99 e54)))
(let ((e161 (or e68 e144)))
(let ((e162 (=> e90 e76)))
(let ((e163 (ite e162 e146 e61)))
(let ((e164 (=> e63 e88)))
(let ((e165 (= e107 e163)))
(let ((e166 (or e77 e62)))
(let ((e167 (ite e64 e159 e91)))
(let ((e168 (not e45)))
(let ((e169 (ite e92 e50 e166)))
(let ((e170 (=> e72 e147)))
(let ((e171 (= e48 e58)))
(let ((e172 (=> e169 e117)))
(let ((e173 (=> e145 e93)))
(let ((e174 (and e51 e164)))
(let ((e175 (or e161 e71)))
(let ((e176 (or e173 e171)))
(let ((e177 (xor e152 e103)))
(let ((e178 (ite e59 e85 e59)))
(let ((e179 (and e65 e155)))
(let ((e180 (or e82 e82)))
(let ((e181 (= e165 e60)))
(let ((e182 (= e167 e149)))
(let ((e183 (not e177)))
(let ((e184 (= e168 e168)))
(let ((e185 (ite e160 e78 e175)))
(let ((e186 (ite e185 e180 e97)))
(let ((e187 (or e56 e178)))
(let ((e188 (= e133 e179)))
(let ((e189 (not e140)))
(let ((e190 (ite e129 e101 e188)))
(let ((e191 (= e172 e190)))
(let ((e192 (xor e186 e186)))
(let ((e193 (not e182)))
(let ((e194 (and e191 e176)))
(let ((e195 (xor e128 e157)))
(let ((e196 (or e151 e151)))
(let ((e197 (not e81)))
(let ((e198 (not e192)))
(let ((e199 (or e197 e187)))
(let ((e200 (xor e150 e183)))
(let ((e201 (or e189 e52)))
(let ((e202 (= e170 e158)))
(let ((e203 (=> e201 e137)))
(let ((e204 (=> e198 e193)))
(let ((e205 (=> e202 e184)))
(let ((e206 (=> e195 e174)))
(let ((e207 (or e98 e205)))
(let ((e208 (= e196 e200)))
(let ((e209 (or e199 e153)))
(let ((e210 (or e203 e143)))
(let ((e211 (=> e208 e209)))
(let ((e212 (=> e210 e206)))
(let ((e213 (= e181 e211)))
(let ((e214 (and e194 e207)))
(let ((e215 (and e213 e212)))
(let ((e216 (and e204 e215)))
(let ((e217 (or e216 e214)))
(let ((e218 (and e217 (not (= e13 (_ bv0 128))))))
(let ((e219 (and e218 (not (= e13 (bvnot (_ bv0 128)))))))
e219
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
